1 Introduction

Welcome to Process Analysis Toolkit (PAT)!

PAT is a self-contained framework for to support composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g. partial order reduction, symmetry reduction, process counter abstraction, parallel model checking.

The main functionalities of PAT are listed as follows:

User friendly editing environment (multi-document, multi-language, I18N GUI and advanced syntax editing features) for introducing models
User friendly simulator for interactively and visually simulating system behaviors; by random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
Easy verification for deadlock-freeness analysis, reachability analysis, state/event linear temporal logic checking (with or without fairness) and refinement checking.
A wide range of built-in examples ranging from benchmark systems to newly developed algorithms/protocols.

We design PAT as an extensible and modularized framework, which allows user to build customized model checkers easily. We provide a library of model checking algorithms as well as the support for customizing language syntax, semantics, model checking algorithms and reduction techniques, graphic user interfaces, and domain specific abstraction techniques. Delightfully, PAT has been growing up to eleven modules today to deal with problems in different domains including Real Time Systems, Web Service Models, Probability Models, and Sensor Networks etc. In order to be state-of-the-art, we are actively developing PAT to cope with latest formal-automated system analysis techniques.

We have been using PAT to model and verify a variety of systems. Ranging from recently proposed distributed algorithms, security protocols to real-world systems like multi-lift and pacemaker systems. Previously unknown bugs have been discovered. The experiment results (available in PAT web site) show that PAT is capable of verifying systems with large number of states and outperforms the popular model checkers in some cases. We have successfully demonstrated PAT as an analyzer for process algebras in the 30th International Conference on Software Engineering (ICSE 2008) [LiuSD08], the 21st International Conference on Computer Aided Verification (CAV 2009) [SunLDP09] and FSE 2010 [LIUSD10].

This manual will introduce you various aspects of PAT, including using PAT and specific knowledge of different modules in PAT. In this chapter, we will discuss about why we need system verification and what PAT is designed for. See Section 1.1 Preface. Also we will give an outline to show how this manual is organized and what are the main topics covered. See Section1.2 Organization.

About PAT:

PAT project is initialized in School of Computing, National University of Singapore in July 2007.

The key members designing PAT are:

Dr. SUN, Jun, Assistant Professor, Singapore University of Technology and Design.
Dr. LIU, Yang, Senior Research Scientist, Temasek Laboratories and School of Computing, National University of Singapore.
Dr. DONG, Jin Song, Associated Professor, School of Computing, National University of Singapore.

Contact us:

Should you meet any difficulty using PAT or find bugs of PAT or have some suggestion on improving PAT, please do not hesitate to contact any one of us. Alternatively, you can send an email to pat@comp.nus.edu.sg.

Acknowledgement

We own thanks to research collaborators, including Prof. Jun Pang, Prof. Hai Wang, Prof. Jing Sun, Prof. Wei Chen, Prof. Annie Y. Liu and Prof. Geguang Pu.

We would like to thank Prof. Jing Sun, Prof. Hugh Anderson, Prof. Jonathan S. Ostroff for using PAT for the course teaching. Their valuable feedback made PAT more suitable for teaching.

We are very grateful for the valuable comments and suggestions from professor Tony Hoare, professor Joxan Jaffar, professor Jim Woodcock, professor Jim Davis, professor Jens Palsberg, professor Auguston Mikhail, professor Kokichi FUTATSUGI, professor Phil Brooke, professor Kenji Taguchi, professor Doron A. Peled so on.

We have special thanks to our Japanese user group, especially Hiroshi Fujimoto, Kenji Taguchi, Masaru Nagaku, Toshiyuki Fujikura.